Inference at * 
Iof proof for Lemma can-apply-fun-exp-add-iff:


  A:Type, n, m:, f:(A(A + Top)), x:A.
  (can-apply(f^n+m;x))  ((can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x)))) 

latex

 by ((((UnivCD) 
CollapseTHENA (Auto))) 
CCollapseTHEN ((if (((first_nat 2:n
CC)) = 0) then (Repeat (((D (0)) 
CollapseTHENA (MaAuto)))) else (RepeatFor (first_nat 2:n) (((
CoD (0)) 
CollapseTHENA (MaAuto))))))) 

latex

Co1: 

Co1: 1. A : Type
Co1: 2. n : 
Co1: 3. m : 
Co1: 4. f : A(A + Top)
Co1: 5. x : A
Co1: 6. can-apply(f^n+m;x)
Co1:   (can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x)))
Co2: 

Co2: 1. A : Type
Co2: 2. n : 
Co2: 3. m : 
Co2: 4. f : A(A + Top)
Co2: 5. x : A
Co2: 6. (can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x)))
Co2:   can-apply(f^n+m;x)
Co.

Definitions	P  Q, suptype(S; T), S  T, x:A. B(x), Void, a < b, n+m, , A, False, A  B, P  Q, P  Q, x:A  B(x), P & Q, A c B, , can-apply(f;x), f^n, Top, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), {x:A| B(x)} , b, x:AB(x), left + right, , Type, t  T, s = t
Lemmas	iff wf, can-apply wf, p-fun-exp wf, top wf, nat wf, member wf, le wf, rev implies wf, assert wf